﻿// ==++==
// 
//   Copyright (c) Microsoft Corporation.  All rights reserved.
// 
// ==--==
using System;
using System.Collections.Generic;
using System.IO;
using System.Text;
using Microsoft.ExtendedReflection.Collections;
using Microsoft.ExtendedReflection.ComponentModel;
using Microsoft.ExtendedReflection.Interpretation;
using Microsoft.ExtendedReflection.Interpretation.Interpreter;
using Microsoft.ExtendedReflection.Logging;
using Microsoft.ExtendedReflection.Metadata;
using Microsoft.ExtendedReflection.Metadata.Names;
using Microsoft.ExtendedReflection.Reasoning.ExecutionNodes;
using Microsoft.Pex.Engine.SearchFrontiers;
using Microsoft.ExtendedReflection.Utilities;
using Microsoft.ExtendedReflection.Utilities.Safe.Diagnostics;
using Microsoft.Pex.Engine.ComponentModel;
using Microsoft.Pex.Engine.Packages;
using Microsoft.Pex.Framework.ComponentModel;
using Microsoft.Pex.Engine.PathExecution;
using Microsoft.Pex.Framework.Packages;
using Microsoft.Pex.Fitness.Implementation;
using Microsoft.Pex.Fitness.Interfaces;
using Microsoft.ExtendedReflection.Interpretation.Interpreter.Monitoring;

namespace Microsoft.Pex.Fitness
{
    [__DoNotInstrument]
    public sealed partial class PexSearchFrontierFittestFirstAttribute
        : PexComponentElementDecoratorAttributeBase
        , IPexExplorationPackage
        , IPexPathPackage
    {
        const bool logging = false;
        const bool loggingVerbose = false;

        #region generation configuration options
        public PexFitnessStrategyKind Strategy = PexFitnessStrategyKind.AlternateForTargets;
        const bool useBranchFitnessGain = true;
        #endregion

        public PexSearchFrontierFittestFirstAttribute() { }

        #region IPexExplorationPackage Members

        string IPexExplorationPackage.Name
        {
            get { return "FitnessExplorationPackage"; }
        }

        public bool IsRoundRobin;

        void IPexExplorationPackage.Load(
            IContainer explorationContainer)
        {
            explorationContainer.AddComponent(
                null, new PexFitnessExplorationManager(this.Strategy, logging, loggingVerbose, useBranchFitnessGain));
        }

        void IPexExplorationPackage.Initialize(IPexExplorationEngine host)
        {
            IPexSearchFrontierManager sfm = host.GetService<IPexSearchFrontierManager>();
            sfm.DontUseFittestFrontier = true;
            var searchFrontierFactory = (Factory<IPexSearchFrontier>)delegate()
                {
                    Random random = new Random(0);
                    var builtinSearchFrontiers = host.GetService<IPexBuiltinSearchFrontiers>();
                    IPexSearchFrontier defaultFrontier;
                    if (this.IsRoundRobin)
                        defaultFrontier = null;
                    else
                        defaultFrontier = builtinSearchFrontiers.DefaultRoundRobin(random, null, false);
                    IPexSearchFrontier fitnessFrontier;
                    PexLocatedInnerFrontierFactory<int> innerFrontierFactory =
                        fitness =>
                            builtinSearchFrontiers.Alternate(
                                builtinSearchFrontiers.CallStackTracePrioritized(random, callStack => builtinSearchFrontiers.IterativeDeepening(random)),
                                builtinSearchFrontiers.CodeLocationPrioritized(random, null, codeLocation => builtinSearchFrontiers.IterativeDeepening(random)));

                    switch (this.Strategy)
                    {
                        case PexFitnessStrategyKind.OverallMinFitnessValueForAllTargets:
                            fitnessFrontier = new PexFitnessFrontierBase.OverallMinFitnessValueForAllTargets(
                                host, random, innerFrontierFactory, defaultFrontier);
                            break;
                        case PexFitnessStrategyKind.AlternateForTargets:
                            fitnessFrontier = new PexFitnessFrontierBase.AlternateForTargets(
                                host, random, innerFrontierFactory, defaultFrontier);
                            break;
                        default:
                            throw SafeDebug.FatalFailOnUnexpectedValue<PexFitnessStrategyKind>(this.Strategy);
                    }
                    return fitnessFrontier;
                };
            if (this.IsRoundRobin)
                sfm.AddRoundRobinSearchFrontier(searchFrontierFactory);
            else
                sfm.SetMainSearchFrontier(searchFrontierFactory);
        }

        object IPexExplorationPackage.BeforeExploration(IPexExplorationComponent host)
        {
            return null;
        }

        void IPexExplorationPackage.AfterExploration(IPexExplorationComponent host, object data)
        {
        }

        #endregion

        #region IPexPathPackage Members

        string IPexPathPackage.Name
        {
            get { return "FitnessPathPackage"; }
        }

        void IPexPathPackage.Load(IContainer pathContainer)
        {
            pathContainer.AddComponent(
                null, new PexFitnessPathManager());
        }

        object IPexPathPackage.BeforeRun(IPexPathComponent host)
        {
            return host.GetService<IPexFitnessPathManager>(); 
        }

        void IPexPathPackage.AfterRun(IPexPathComponent host, object data)
        {
            var fitnessPathMonitor = (IPexFitnessPathManager)data;
            fitnessPathMonitor.OnPathFinished();
        }

        #endregion

        protected override void Decorate(Name location, IPexDecoratedComponentElement host)
        {
            SafeDebug.AssumeNotNull(location, "location");
            SafeDebug.AssumeNotNull(host, "host");

            host.AddExplorationPackage(location, this);
            host.AddPathPackage(location, this);
        }
    }
}